#ifndef MODEL_HH_
# define MODEL_HH_

///
/// \file Model.hh
/// \brief Class that represent the kripke structure.
/// \author Coddy Levi, Sylvain Lobry
/// \version 1.0
///
///
///

#include <bdd.h>

#include <map>
#include <string>
#include <istream>

///
/// \class Model
/// \brief Kripke structure representation and operations.
///
class Model
{
public:
  ///
  /// \brief parse a kripke structure from an input stream
  ///
  /// \param[in]	in The input stream in which to parse
  ///
  ///
  void parse_model(std::istream& in);

  ///
  /// \brief Parse the number of states present in the stream
  ///
  /// \param[in]	in The input stream in which to parse
  ///
  /// \return		the number of states
  ///
  static int parse_size(std::istream& in);

  ///
  /// \brief Compute the number of bdd variables necessary to represent
  /// a given number of states
  ///
  /// \param[in]	nb_nodes The kripke structure's number of states
  ///
  /// \return		The number of necessary variables
  ///
  static int compute_nb_variables(int nb_nodes);

  ///
  /// \brief Get the BuDDy ID of a problem variable from its name in
  /// the kripke structure's file
  ///
  /// \param[in]	var The variable's name
  ///
  /// \return		The BuDDy ID of the variable
  ///
  int get_problem_variable_index(const std::string& var) const;

  ///
  /// \brief Setter to nb_state_variables
  ///
  /// \param[in]	n The new number of state variables
  ///
  void set_nb_state_variables(int n) { nb_state_variables = n; };

  ///
  /// \brief Inverse all the variables of a state
  ///
  /// \param[in]	state the bdd representing the state's ID
  ///
  /// \return		the inverse bdd
  ///
  bdd reverse_state(bdd state) const;

  ///
  /// \brief compute a bdd representing a given state
  ///
  /// \param[in]	state_number the given state's ID
  ///
  /// \return		the resulting bdd
  ///
  bdd unreverse_state(bdd state) const;

  ///
  /// \brief A special bdd state used in bdd operations
  ///
  /// \return		the bdd in which all variables are true
  ///
  bdd get_state_high() const;

  ///
  /// \brief Accessor to the labelling variables bdd
  ///
  /// \return		the resulting bdd
  ///
  bdd get_problem_variables() const;

  ///
  /// \brief compute a bdd representing a given state
  ///
  /// \param[in]	state_number the given state's ID
  ///
  /// \return		the resulting bdd
  ///
  bdd make_state(int state_number) const;

  ///
  /// The bdd representing the transitions between states
  ///
  bdd successor_relation;

  ///
  /// The bdd representing the states' labels
  ///
  bdd label_relation;
private:

  ///
  /// \brief Parse a kripke structure state from an input stream
  ///
  /// \param[in]	in the input state in which to parse
  ///
  void parse_state(std::istream& in);

  ///
  /// \brief Parse a state's labelling variables
  ///
  /// \param[in]	in the input state in which to parse
  ///
  /// \return		the variables represented by a bdd
  ///
  bdd parse_variables(std::istream& in);

  ///
  /// \brief Parse a kripke structure state's transitions
  ///
  /// \param[in]	in the input state in which to parse
  ///
  /// \return		the successor relations represented by a bdd
  ///
  bdd parse_successors(std::istream& in);

  typedef std::map<std::string, int> t_var_map;

  ///
  /// Mapping between a var's name and its buDDy ID
  ///
  t_var_map problem_variables;

  ///
  /// Number of variables used to describe a state ID
  ///
  int nb_state_variables;

  ///
  /// Number of "problem" variables used to label the states
  ///
  int nb_problem_variables;
};

#endif /* !MODEL_HH_ */
